#include "refactor.h"

//--- Local Type definition
typedef ushort len_t;
// s>6?(1<<(s-6)):1; 
static const unsigned short truth_table_length[13] ={0,1,1,1,1,1,1,2,4,8,16,32,64};
//=============================================================================
//     BASIC TRUTH TABLE ARITHMETIC
//=============================================================================
static void sim( len_t s , const bool_t a , const bool_t b , unsigned sig , bool_t o )
{
   switch( sig )
   {
      case 0 :  for( int i = 0 ; i < s ; ++ i )o[i] = ( a[i]  &   b[i]) ; break ;
      case 1 :  for( int i = 0 ; i < s ; ++ i )o[i] = ( a[i]) & (~b[i]) ; break ;
      case 2 :  for( int i = 0 ; i < s ; ++ i )o[i] = (~a[i]) & ( b[i]) ; break ; 
      case 3 :  for( int i = 0 ; i < s ; ++ i )o[i] = (~a[i]) & (~b[i]) ; break; 
   }
}
//=============================================================================
//      CONSTRUCTOR AND DESCTRUCTOR
//=============================================================================
Refactor::Refactor( )
   : _cutSize(0), INV(false)
{
   //--- initial cone size allocation 
   _cone.growTo( 100 );
   _cone.clear();
   
   table_allocate( 128 ); 

   for( int i = 0 ; i < 6 ; ++i )
   {
      uint64_t b = ((uint64_t)1<<(1<<i))-1;
      for( int j = i+1 ; j < 6 ; ++ j )
         b |= b<<(1<<j);

      bool_t t = _tables[i];

      for( int j = 0 ; j < TABLE_SIZE ; ++ j )
         t[j] = b;

      t = _tables[i+6];
      for( int j = 0 ; j < TABLE_SIZE ; ++ j)
         if( (b >> j) & 1 ) t[j] = -1; 
         else               t[j] =  0;
   }

   _mem_start = new unsigned [ RF_MEM_SIZE ];
}
Refactor::~Refactor( )
{
   for( unsigned i = 0 ; i < _truth_table_pages.size() ; ++ i ) 
      delete [] _truth_table_pages[i];
   delete [] _mem_start;
}
//=============================================================================
//     UN classified function  
//=============================================================================
void  Refactor::table_allocate( unsigned n )
{
   uint64_t * p = new uint64_t[ n * TABLE_SIZE ];   assert( p );
   _truth_table_pages.push( p );
   for( unsigned i = 0 ; i < n ; ++ i ) 
   {
      _tables.push( bool_t( p ) );
      p += TABLE_SIZE;
   }
}
void Refactor::rf_simulate() 
{
   for( unsigned i = 0 ; i < _cutSize ; ++i ) 
      _funmap[ _cut[i] ] = i;

   _fun_length = truth_table_length[ _cutSize ];

   {
      int n = _cone.size() + 12 - _tables.size();
      if( n >= 0 ) table_allocate( n );
   }

   for( int i = _cone.size() -1 ; i >= 0 ; -- i)
   {
      unsigned n = _cone[i];
      AigLit in[2] = { eqIn(n,0) , eqIn(n,1) };
      _funmap[ n ] = i + 12 ;
      sim( _fun_length , _tables[ _funmap[ var(in[0]) ] ],_tables[ _funmap[ var(in[1]) ] ], 
            ( sign(in[0]) << 1) | sign(in[1])  , _tables[ i + 12 ]  );
   }
}
//=============================================================================
//      CONE COLLECTION AND CONSTRUCT
//=============================================================================
// get the convergence cut
unsigned Refactor::rf_get_cut( unsigned idx  )
{
   unsigned * focnt   = _focnt.data;
   mark_t   * mrk     = _mrk.data;
   unsigned   andFlag = _andFlag;

   _cone.clear();

   // stage 1 , minimal mffc must larger than 1 
    
   _cut[ 0 ] = idx;
   _cut[ 12 ] = 0;
   _cutSize = 1 ;
   mrk[ idx ] = true;

   do
   {
      // select a cut with min cost 
      int mincost = -1;

      unsigned * sel;

      for( unsigned * i = _cut ; i != _cut + _cutSize ; ++i )
      {
         if( *i < andFlag || focnt[ *i ]) continue;

         int cost = mrk[ eqInIdx( *i , 0 ) ] + 
                    mrk[ eqInIdx( *i , 1 ) ];

         if( cost > mincost || (cost == mincost &&  *sel < *i ) )
            // selecting larger cost or larger index  
            sel = i , mincost = cost;
      }
      if( mincost < 0 || (mincost==0&&_cutSize==RF_CUT_LIMIT)) break;
      	
      unsigned node[2] = { eqInIdx( *sel , 0 ) , eqInIdx( *sel ,1 ) };
      _cone.push( *sel );

      // expand the cut 
      if( mincost == 2 )
      {
         * sel = _cut[ -- _cutSize ] ;
      }
      else if( mincost == 1 )
      {
         * sel = mrk[ node[0] ] ? node[1] : node[0];
      }
      else
      {
         *sel = node[0];
         _cut[ _cutSize ++ ] = node[1];
      }

      focnt[ node [0] ] -=1;
      focnt[ node [1] ] -=1;
      mrk[ node[0] ] = mrk[ node[1] ] = true;

   }while(1);
   
   for( unsigned i = 0 ; i < _cutSize ; ++ i ) 
      mrk[ _cut[i] ] = false;
   for( unsigned i = 0 ; i < _cone.size() ; ++i )
      mrk[ _cone[i] ] = false;

   return _cone.size();
}
unsigned Refactor::rf_count_cost( unsigned n )
{
   validation();
   _funmap.growTo( size() );

   mark_t   * mrk     = _mrk.data;
   unsigned * focnt = _focnt.data;
   unsigned   andFlag = _andFlag;

   for( unsigned i = 0 ; i < _cutSize ; ++ i ) 
      mrk[ _cut[i] ] = true;

   _build_cone.clear();

   if( focnt[n] == 0 && ! mrk[n] )
   {
      unsigned ptr = 0;
      mrk[ n ] = true;
      _build_cone.push(n);
      
      while( _build_cone.size() != ptr )
      {
         unsigned node = _build_cone[ptr++];
         if( node < andFlag ) continue;
         for( unsigned j = 0 ; j < 2 ; ++ j )
         {
            n = eqInIdx( node , j ); 
            if( focnt[ n ] == 0 && ! mrk[ n ] )
               _build_cone.push( n ) , mrk[ n ] = true;
         }
      }
      for( unsigned i = 0 ; i < _build_cone.size() ; ++i )
         mrk[ _build_cone[i] ] = false; 
   }
   for( unsigned i = 0 ; i < _cutSize ; ++ i ) 
      mrk[ _cut[i] ] = false;

   return _build_cone.size();
}
void Refactor::build_cone()
{
   unsigned * focnt = _focnt.data;
   for( unsigned i = 0 ; i < _build_cone.size() ; ++ i )
   {
      unsigned n = _build_cone[i];
      focnt[ eqInIdx(n,0) ] +=1;
      focnt[ eqInIdx(n,1) ] +=1;
   }
}
void Refactor::resume()
{
   unsigned * focnt = _focnt.data;
   for( unsigned i = 0 ; i < _cone.size() ; ++ i )
   {
      unsigned n = _cone[i];
      focnt[ eqInIdx(n,0) ] +=1;
      focnt[ eqInIdx(n,1) ] +=1;
   }
}
//=============================================================================
//      RUN RUN RUN
//=============================================================================
// given a node index perform the refactor
void Refactor::inv_fun( unsigned t )
{
   bool_t b = getfun(t);
   for( unsigned i = 0 ; i < _fun_length ; ++i ) b[i] = ~b[i];
}
void Refactor::run( unsigned idx )
{ 
   if( todo(idx)==false)return;
   unsigned focnt = 0;

   // get the cut 
   std::swap( _focnt[idx] , focnt );
   unsigned mffc = rf_get_cut( idx );
   
   // compute function of the node 
   rf_simulate();
   
   // fun == 0 or 1 return 
   // composing it into ISOP
   _mem = _mem_start;
   if( INV ) inv_fun( idx );
   unsigned k = Morreale_Minato_ISOP( getfun(idx),getfun(idx),_fun_length/2,_mem );
   if( k >= RF_MAX_SOP_SIZE ) { resume() ; std::swap( _focnt[idx] , focnt ); return; } 
   cube_t f   = allocate_cube( k );

   // adding this line would not decrease performance but avoid mem blow up
   _size = size();
   unsigned p = var( qfactor( f ) );
   unsigned cost = rf_count_cost( p );

   if( mffc >= cost && accept( idx , p ) ) 
   {
      resume();
      replace( idx , p , focnt );
   }else
   {
      resume();
      std::swap( _focnt[idx] , focnt );
      while( _size != size() ) pop_back();
      validation();
   }
}
void Refactor::init()
{
   _funmap.growTo( sz );
   CktInfo::init();
} 
void Refactor::run()
{
   unsigned size = sz;
   for( unsigned i = _andFlag ; i < size ; ++ i )
   {
      if( _focnt[ i ] == 0 ) continue;
      run( i );
   }
}

